Nuprl Definition : fun-connected
11,40
postcript
pdf
y
is
f
*(
x
) ==
L
:
T
List.
y
=
f
*(
x
) via
L
latex
clarification:
fun-connected(
T
;
f
;
x
;
y
) ==
L
:
T
List. fun-path(
T
;
f
;
L
;
y
;
x
)
latex
Definitions
x
:
A
.
B
(
x
)
,
type
List
,
y
=
f
*(
x
) via
L
FDL editor aliases
fun-connected
origin
L:T List. y=f*(x) via L
L:T List. fun-path(T;f;L;y;x) L:T List. y=f*(x) via L
L:T List. fun-path(T;f;L;y;x) x:A. B(x)